A tool for statically checking C source code